
/* 
  This assignment illustrates how specifications (esp invariants and 
  preconditions)  written in a formal language can help in removing 
  errors in code. 

  The assignment concerns a class "Taxpayer" that is used for taxpayers.

  (C) Erik Poll
 */
class Taxpayer {

 /* FIELDS */
	
 /* isFemale is true iff the person is female */
 boolean isFemale;

 /* isMale is true iff the person is male */
 boolean isMale;


 Taxpayer father, mother; // These fields won't really be used until
                          // the next part of the exercise.

 /* Age in years */ 
 int age; 

 boolean isMarried; 

 /* Reference to spouse if person is married, null otherwise */
 Taxpayer spouse; 
 
 /*--------------- INVARIANTES DE CLASE -------------------------*/
  // PARTE 1 ------------------------------------------------------
	//@ invariant this.isFemale <==> ! this.isMale;
	//@ invariant this.isMarried <==> (this.spouse != null);
	//@ invariant this.isMarried ==> (this.isMale <==> this.spouse.isFemale);
	//@ invariant this.isMarried ==> (this.spouse.isMarried); 
	//@ invariant this.isMarried ==> (this.spouse.spouse == this);
  // PARTE 2 ------------------------------------------------------
	// El siguiente puede no ir
	//@ invariant tax_allowance >= 0;
  // PARTE 3 -----------------------------------------------------
	//@ invariant (!this.isMarried && this.age < 65) ==> (this.tax_allowance == DEFAULT_ALLOWANCE);
	//@ invariant (!this.isMarried && this.age >= 65) ==> (this.tax_allowance == ALLOWANCE_OAP);
	//@ invariant (this.isMarried && this.age >= 65 && this.spouse.age >= 65) ==> (this.tax_allowance + this.spouse.tax_allowance == 2 * ALLOWANCE_OAP);
	//@ invariant (this.isMarried && this.age >= 65 && this.spouse.age < 65) ==> (this.tax_allowance + this.spouse.tax_allowance == DEFAULT_ALLOWANCE + ALLOWANCE_OAP);
	//@ invariant (this.isMarried && this.age < 65 && this.spouse.age < 65) ==> (this.tax_allowance + this.spouse.tax_allowance == 2* DEFAULT_ALLOWANCE );
	// El siguiente no lo pide ni es necesario pero se deriva del contexto
	//@ invariant age >= 0;
	
/*---------------------------------------------------------------*/

 /* Constant default income tax allowance (belastingvrije som) */
 static final int DEFAULT_ALLOWANCE = 5000;

 /* Constant income tax allowance for Old Age Pensioners over 65 */
 static final  int ALLOWANCE_OAP = 7000;

 /* Income tax allowance (belastingvrije som) */
 int tax_allowance; 

 /* Income per year */
 int income; 

 /* CONSTRUCTOR */

 Taxpayer(boolean jongetje, Taxpayer ma, Taxpayer pa) {
   age = 0;
   isMarried = false;
   this.isMale = jongetje;
   this.isFemale = !jongetje;
   mother = ma;
   father = pa;
   spouse = null;
   income = 0;
   tax_allowance = DEFAULT_ALLOWANCE;
   /* The line below makes explicit the assumption that a new Taxpayer is not 
    * married to anyone yet. A bit silly of course, but we need this to keep 
    * ESC/Java2 happy. */
   //@ assume (\forall Taxpayer p; p.spouse != this); 
 } 

 /* METHODS */

 /* Marry to new_spouse */
 //@ requires new_spouse != null;
 //@ requires new_spouse.isMale <==> this.isFemale;
 //@ requires (!new_spouse.isMarried);
 //@ requires (!this.isMarried); 
 void marry(Taxpayer new_spouse) {
  spouse = new_spouse;
  new_spouse.spouse = this;
  isMarried = true;
  new_spouse.isMarried = true;
 }
 
 /* Divorce from current spouse */
 //@ requires this.isMarried;
 void divorce() {
  spouse.isMarried = false;
  isMarried = false;
  if (age >= 65 ) {
	tax_allowance = ALLOWANCE_OAP;	
  } else {
	tax_allowance = DEFAULT_ALLOWANCE;
  }
  if (spouse.age >= 65 ) { 
	spouse.tax_allowance = ALLOWANCE_OAP;	
  } else {
	spouse.tax_allowance = DEFAULT_ALLOWANCE;
  }	
  spouse.spouse = null;
  spouse = null;
 }
 

 /* Transfer change of the tax allowance from this person to his/her spouse */
 //@ requires this.isMarried;
 //@ requires change >= 0;
 //@ requires change <= tax_allowance;
 void transferAllowance(int change) {
  tax_allowance = tax_allowance - change;
  spouse.tax_allowance = spouse.tax_allowance + change;
 }

 /* Taxpayer has a birthday and the age increases by one */
 void haveBirthday() {
  age++;
  // no se si esta correccion esta bien (no se si hace lo que se pide)
  if (age == 65) {
	if (isMarried) {
		if (spouse.age >= 65 ) {
			tax_allowance = 2 * ALLOWANCE_OAP - spouse.tax_allowance;
		} else {
			tax_allowance = ALLOWANCE_OAP + DEFAULT_ALLOWANCE - spouse.tax_allowance;
		}
	} else {
		tax_allowance = ALLOWANCE_OAP;
	}
  }
 }

}
